Msg($M$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$l$:IdLnk $\times$ ($t$:Id $\times$ ($M$($l$,$t$)))